#include <klee/klee.h>
#define MIN(x, y) ((x) < (y)) ? (x) : (y)
#define MAX(x, y) ((x) < (y)) ? (y) : (x)

unsigned int gcd(unsigned int x, unsigned int y)
{
    unsigned int k = MAX(x, y);
    unsigned int m = MIN(x, y);

    if (k == 0 && m == 0)
        return 0;

    while (m != 0) {
        unsigned int r = k % m;
        k = m;
        m = r;
    }

    return k;
}

int main(void)
{
    unsigned int a, b;
    klee_make_symbolic(&a, sizeof(a), "a");
    klee_make_symbolic(&b, sizeof(b), "b");
    return gcd(a, b);
}
